Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    active(f(a,b,X))  → mark(f(X,X,X))
2:    active(c)  → mark(a)
3:    active(c)  → mark(b)
4:    active(f(X1,X2,X3))  → f(active(X1),X2,X3)
5:    active(f(X1,X2,X3))  → f(X1,X2,active(X3))
6:    f(mark(X1),X2,X3)  → mark(f(X1,X2,X3))
7:    f(X1,X2,mark(X3))  → mark(f(X1,X2,X3))
8:    proper(f(X1,X2,X3))  → f(proper(X1),proper(X2),proper(X3))
9:    proper(a)  → ok(a)
10:    proper(b)  → ok(b)
11:    proper(c)  → ok(c)
12:    f(ok(X1),ok(X2),ok(X3))  → ok(f(X1,X2,X3))
13:    top(mark(X))  → top(proper(X))
14:    top(ok(X))  → top(active(X))
There are 16 dependency pairs:
15:    ACTIVE(f(a,b,X))  → F(X,X,X)
16:    ACTIVE(f(X1,X2,X3))  → F(active(X1),X2,X3)
17:    ACTIVE(f(X1,X2,X3))  → ACTIVE(X1)
18:    ACTIVE(f(X1,X2,X3))  → F(X1,X2,active(X3))
19:    ACTIVE(f(X1,X2,X3))  → ACTIVE(X3)
20:    F(mark(X1),X2,X3)  → F(X1,X2,X3)
21:    F(X1,X2,mark(X3))  → F(X1,X2,X3)
22:    PROPER(f(X1,X2,X3))  → F(proper(X1),proper(X2),proper(X3))
23:    PROPER(f(X1,X2,X3))  → PROPER(X1)
24:    PROPER(f(X1,X2,X3))  → PROPER(X2)
25:    PROPER(f(X1,X2,X3))  → PROPER(X3)
26:    F(ok(X1),ok(X2),ok(X3))  → F(X1,X2,X3)
27:    TOP(mark(X))  → TOP(proper(X))
28:    TOP(mark(X))  → PROPER(X)
29:    TOP(ok(X))  → TOP(active(X))
30:    TOP(ok(X))  → ACTIVE(X)
The approximated dependency graph contains 4 SCCs: {20,21,26}, {17,19}, {23-25} and {27,29}.
Tyrolean Termination Tool  (1.71 seconds)   ---  May 4, 2006